(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 2))
(let ((e4 1))
(let ((e5 3))
(let ((e6 (/ e5 (- e3))))
(let ((e7 (* v1 v1)))
(let ((e8 (+ e6 e6)))
(let ((e9 (/ e4 e5)))
(let ((e10 (- e7 v0)))
(let ((e11 (- v0)))
(let ((e12 (- v0)))
(let ((e13 (- v0)))
(let ((e14 (- e11)))
(let ((e15 (/ e5 (- e3))))
(let ((e16 (- e15)))
(let ((e17 (* e14 e10)))
(let ((e18 (- e12)))
(let ((e19 (- v0 e13)))
(let ((e20 (* v1 e4)))
(let ((e21 (+ e10 e10)))
(let ((e22 (+ e10 e8)))
(let ((e23 (- e15 e10)))
(let ((e24 (/ e5 e4)))
(let ((e25 (- e18 v1)))
(let ((e26 (/ e5 e3)))
(let ((e27 (- e9 e20)))
(let ((e28 (- e16 e27)))
(let ((e29 (- e9 e13)))
(let ((e30 (* e25 e4)))
(let ((e31 (+ e30 e11)))
(let ((e32 (* (- e4) e15)))
(let ((e33 (- e14)))
(let ((e34 (+ e20 v1)))
(let ((e35 (* v1 e21)))
(let ((e36 (+ e23 e26)))
(let ((e37 (/ e4 e5)))
(let ((e38 (- v2)))
(let ((e39 (= e37 e33)))
(let ((e40 (> e11 e35)))
(let ((e41 (distinct e29 e34)))
(let ((e42 (= e22 e17)))
(let ((e43 (>= e35 e32)))
(let ((e44 (< e31 e21)))
(let ((e45 (> e13 e29)))
(let ((e46 (distinct e16 e38)))
(let ((e47 (distinct e16 e8)))
(let ((e48 (<= v0 e35)))
(let ((e49 (> e23 e8)))
(let ((e50 (> e10 v2)))
(let ((e51 (distinct v0 e18)))
(let ((e52 (< e12 e26)))
(let ((e53 (> e28 e12)))
(let ((e54 (<= e35 e16)))
(let ((e55 (distinct e13 e21)))
(let ((e56 (> e36 e24)))
(let ((e57 (< e28 e22)))
(let ((e58 (< e30 e36)))
(let ((e59 (distinct e11 e7)))
(let ((e60 (< e27 e32)))
(let ((e61 (<= e31 e26)))
(let ((e62 (< e10 e7)))
(let ((e63 (> e30 e20)))
(let ((e64 (distinct e30 e29)))
(let ((e65 (< v2 e36)))
(let ((e66 (>= e22 e26)))
(let ((e67 (> e9 e24)))
(let ((e68 (>= e32 e16)))
(let ((e69 (= e27 e9)))
(let ((e70 (> e8 e6)))
(let ((e71 (distinct e7 e6)))
(let ((e72 (< e18 e24)))
(let ((e73 (< e28 e17)))
(let ((e74 (> e18 e28)))
(let ((e75 (>= v2 e35)))
(let ((e76 (= e20 e17)))
(let ((e77 (> e28 e16)))
(let ((e78 (< e6 e37)))
(let ((e79 (distinct e14 e11)))
(let ((e80 (<= e18 e29)))
(let ((e81 (= e32 e11)))
(let ((e82 (< e20 v1)))
(let ((e83 (< e34 e21)))
(let ((e84 (= e29 e30)))
(let ((e85 (<= e33 e29)))
(let ((e86 (< v0 e35)))
(let ((e87 (= e9 e30)))
(let ((e88 (< e21 e15)))
(let ((e89 (distinct e6 e38)))
(let ((e90 (= e33 e29)))
(let ((e91 (< e19 e17)))
(let ((e92 (< v1 e35)))
(let ((e93 (= e16 e22)))
(let ((e94 (distinct e7 e30)))
(let ((e95 (>= e13 e27)))
(let ((e96 (< e8 e35)))
(let ((e97 (distinct e13 e19)))
(let ((e98 (< e23 e25)))
(let ((e99 (<= e26 e32)))
(let ((e100 (> v0 e16)))
(let ((e101 (<= e16 e10)))
(let ((e102 (> v2 e19)))
(let ((e103 (>= e16 v0)))
(let ((e104 (> e10 e32)))
(let ((e105 (> v2 v2)))
(let ((e106 (distinct e14 e17)))
(let ((e107 (<= e9 e21)))
(let ((e108 (>= e21 e10)))
(let ((e109 (= v2 v1)))
(let ((e110 (< e38 e36)))
(let ((e111 (= e23 e29)))
(let ((e112 (> e18 e33)))
(let ((e113 (distinct e18 v2)))
(let ((e114 (distinct e25 e10)))
(let ((e115 (< e28 e25)))
(let ((e116 (< e29 e10)))
(let ((e117 (distinct e26 e37)))
(let ((e118 (>= e8 e20)))
(let ((e119 (< e6 e30)))
(let ((e120 (< e13 e27)))
(let ((e121 (< e21 e32)))
(let ((e122 (distinct e17 e7)))
(let ((e123 (<= e7 e7)))
(let ((e124 (= e11 e12)))
(let ((e125 (distinct e8 e9)))
(let ((e126 (< v0 e15)))
(let ((e127 (< e18 v0)))
(let ((e128 (<= e21 e17)))
(let ((e129 (= e8 e16)))
(let ((e130 (<= e26 v1)))
(let ((e131 (<= e11 e28)))
(let ((e132 (= e30 e10)))
(let ((e133 (> e21 e21)))
(let ((e134 (= e28 e13)))
(let ((e135 (>= e25 e27)))
(let ((e136 (= v2 e14)))
(let ((e137 (> e13 e38)))
(let ((e138 (distinct e10 e30)))
(let ((e139 (> e29 e31)))
(let ((e140 (<= e21 e11)))
(let ((e141 (distinct v1 v1)))
(let ((e142 (< e10 e35)))
(let ((e143 (> e34 e35)))
(let ((e144 (distinct e34 e24)))
(let ((e145 (= e30 e23)))
(let ((e146 (<= e32 e24)))
(let ((e147 (>= v1 e9)))
(let ((e148 (< e10 e29)))
(let ((e149 (distinct e24 e17)))
(let ((e150 (distinct e25 e21)))
(let ((e151 (< e6 e15)))
(let ((e152 (distinct e12 v1)))
(let ((e153 (> e36 e30)))
(let ((e154 (distinct e30 e25)))
(let ((e155 (< e13 e20)))
(let ((e156 (>= e27 e16)))
(let ((e157 (>= e21 e30)))
(let ((e158 (= v0 e31)))
(let ((e159 (>= e19 e36)))
(let ((e160 (distinct e32 e31)))
(let ((e161 (= e27 e22)))
(let ((e162 (not e135)))
(let ((e163 (=> e87 e127)))
(let ((e164 (xor e81 e81)))
(let ((e165 (ite e93 e144 e110)))
(let ((e166 (not e105)))
(let ((e167 (not e143)))
(let ((e168 (ite e109 e126 e88)))
(let ((e169 (not e102)))
(let ((e170 (or e106 e151)))
(let ((e171 (=> e89 e124)))
(let ((e172 (=> e113 e48)))
(let ((e173 (ite e164 e62 e154)))
(let ((e174 (xor e51 e50)))
(let ((e175 (or e74 e139)))
(let ((e176 (and e46 e86)))
(let ((e177 (=> e172 e175)))
(let ((e178 (and e163 e146)))
(let ((e179 (ite e167 e94 e111)))
(let ((e180 (or e56 e133)))
(let ((e181 (ite e180 e141 e66)))
(let ((e182 (xor e118 e52)))
(let ((e183 (or e128 e134)))
(let ((e184 (xor e39 e158)))
(let ((e185 (not e132)))
(let ((e186 (=> e179 e54)))
(let ((e187 (or e131 e121)))
(let ((e188 (or e82 e176)))
(let ((e189 (or e45 e59)))
(let ((e190 (=> e136 e73)))
(let ((e191 (= e155 e115)))
(let ((e192 (xor e53 e178)))
(let ((e193 (= e173 e63)))
(let ((e194 (= e90 e90)))
(let ((e195 (not e114)))
(let ((e196 (xor e100 e40)))
(let ((e197 (and e174 e159)))
(let ((e198 (ite e43 e97 e64)))
(let ((e199 (not e104)))
(let ((e200 (not e181)))
(let ((e201 (or e200 e194)))
(let ((e202 (and e55 e170)))
(let ((e203 (=> e60 e157)))
(let ((e204 (or e95 e192)))
(let ((e205 (xor e42 e72)))
(let ((e206 (not e142)))
(let ((e207 (and e79 e148)))
(let ((e208 (or e103 e61)))
(let ((e209 (and e80 e108)))
(let ((e210 (xor e190 e205)))
(let ((e211 (or e92 e184)))
(let ((e212 (and e169 e117)))
(let ((e213 (=> e168 e76)))
(let ((e214 (= e189 e138)))
(let ((e215 (not e171)))
(let ((e216 (xor e122 e85)))
(let ((e217 (=> e207 e101)))
(let ((e218 (and e41 e49)))
(let ((e219 (xor e140 e96)))
(let ((e220 (or e212 e202)))
(let ((e221 (xor e83 e120)))
(let ((e222 (not e182)))
(let ((e223 (= e222 e162)))
(let ((e224 (xor e69 e197)))
(let ((e225 (or e68 e44)))
(let ((e226 (and e99 e208)))
(let ((e227 (ite e47 e183 e123)))
(let ((e228 (not e188)))
(let ((e229 (ite e210 e149 e214)))
(let ((e230 (or e215 e75)))
(let ((e231 (xor e147 e187)))
(let ((e232 (ite e186 e160 e230)))
(let ((e233 (ite e58 e193 e98)))
(let ((e234 (not e57)))
(let ((e235 (and e216 e137)))
(let ((e236 (or e130 e218)))
(let ((e237 (and e196 e224)))
(let ((e238 (xor e227 e198)))
(let ((e239 (= e67 e116)))
(let ((e240 (not e65)))
(let ((e241 (=> e84 e161)))
(let ((e242 (ite e225 e191 e119)))
(let ((e243 (= e112 e234)))
(let ((e244 (= e231 e239)))
(let ((e245 (or e71 e77)))
(let ((e246 (=> e223 e107)))
(let ((e247 (ite e70 e156 e156)))
(let ((e248 (=> e226 e206)))
(let ((e249 (=> e195 e228)))
(let ((e250 (ite e219 e150 e241)))
(let ((e251 (or e246 e91)))
(let ((e252 (=> e165 e233)))
(let ((e253 (=> e78 e152)))
(let ((e254 (ite e238 e221 e204)))
(let ((e255 (ite e236 e235 e129)))
(let ((e256 (=> e199 e232)))
(let ((e257 (=> e220 e125)))
(let ((e258 (and e245 e250)))
(let ((e259 (xor e229 e240)))
(let ((e260 (and e244 e177)))
(let ((e261 (not e247)))
(let ((e262 (or e237 e252)))
(let ((e263 (ite e203 e248 e217)))
(let ((e264 (and e209 e153)))
(let ((e265 (ite e243 e251 e211)))
(let ((e266 (ite e262 e256 e264)))
(let ((e267 (and e261 e259)))
(let ((e268 (= e185 e213)))
(let ((e269 (not e260)))
(let ((e270 (= e253 e254)))
(let ((e271 (=> e242 e145)))
(let ((e272 (or e258 e265)))
(let ((e273 (or e166 e268)))
(let ((e274 (and e269 e272)))
(let ((e275 (not e271)))
(let ((e276 (ite e270 e274 e249)))
(let ((e277 (= e263 e257)))
(let ((e278 (=> e201 e267)))
(let ((e279 (not e273)))
(let ((e280 (not e277)))
(let ((e281 (xor e276 e280)))
(let ((e282 (not e278)))
(let ((e283 (or e255 e282)))
(let ((e284 (xor e283 e275)))
(let ((e285 (=> e284 e279)))
(let ((e286 (or e285 e281)))
(let ((e287 (not e266)))
(let ((e288 (not e286)))
(let ((e289 (xor e287 e287)))
(let ((e290 (and e289 e289)))
(let ((e291 (not e290)))
(let ((e292 (= e291 e288)))
e292
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
